\functions {
int x0__0;
int x0;
int x0_0;
int x0_1;
int x0_2;
int x0_3;
int x0_4;
int x0_5;
int x0_6;
int x0_7;
int x0_8;
int x0_9;
int x0__1;
int x0__2;
int x0__3;
int x0__4;
int x0__5;
int x0__6;
int x0__7;
int x0__8;
int x0__9;
int x1;
int x1__0;
int x1_0;
int x10;
int x10__0;
int x10_0;
int x10_1;
int x10_2;
int x10_3;
int x10_4;
int x10_5;
int x10_6;
int x10_7;
int x10_8;
int x10_9;
int x10__1;
int x10__2;
int x10__3;
int x10__4;
int x10__5;
int x10__6;
int x10__7;
int x10__8;
int x10__9;
int x11;
int x11__0;
int x11_0;
int x11_1;
int x11_2;
int x11_3;
int x11_4;
int x11_5;
int x11_6;
int x11_7;
int x11_8;
int x11_9;
int x11__1;
int x11__2;
int x11__3;
int x11__4;
int x11__5;
int x11__6;
int x11__7;
int x11__8;
int x11__9;
int x12;
int x12__0;
int x12_0;
int x12_1;
int x12_2;
int x12_3;
int x12_4;
int x12_5;
int x12_6;
int x12_7;
int x12_8;
int x12_9;
int x12__1;
int x12__2;
int x12__3;
int x12__4;
int x12__5;
int x12__6;
int x12__7;
int x12__8;
int x12__9;
int x13;
int x1_1;
int x1_2;
int x1_3;
int x1_4;
int x1_5;
int x1_6;
int x1_7;
int x1_8;
int x1_9;
int x1__1;
int x1__2;
int x1__3;
int x1__4;
int x1__5;
int x1__6;
int x1__7;
int x1__8;
int x1__9;
int x2;
int x2__0;
int x2_0;
int x2_1;
int x2_2;
int x2_3;
int x2_4;
int x2_5;
int x2_6;
int x2_7;
int x2_8;
int x2_9;
int x2__1;
int x2__2;
int x2__3;
int x2__4;
int x2__5;
int x2__6;
int x2__7;
int x2__8;
int x2__9;
int x3;
int x3__0;
int x3_0;
int x3_1;
int x3_2;
int x3_3;
int x3_4;
int x3_5;
int x3_6;
int x3_7;
int x3_8;
int x3_9;
int x3__1;
int x3__2;
int x3__3;
int x3__4;
int x3__5;
int x3__6;
int x3__7;
int x3__8;
int x3__9;
int x4;
int x4__0;
int x4_0;
int x4_1;
int x4_2;
int x4_3;
int x4_4;
int x4_5;
int x4_6;
int x4_7;
int x4_8;
int x4_9;
int x4__1;
int x4__2;
int x4__3;
int x4__4;
int x4__5;
int x4__6;
int x4__7;
int x4__8;
int x4__9;
int x5;
int x5__0;
int x5_0;
int x5_1;
int x5_2;
int x5_3;
int x5_4;
int x5_5;
int x5_6;
int x5_7;
int x5_8;
int x5_9;
int x5__1;
int x5__2;
int x5__3;
int x5__4;
int x5__5;
int x5__6;
int x5__7;
int x5__8;
int x5__9;
int x6;
int x6__0;
int x6_0;
int x6_1;
int x6_2;
int x6_3;
int x6_4;
int x6_5;
int x6_6;
int x6_7;
int x6_8;
int x6_9;
int x6__1;
int x6__2;
int x6__3;
int x6__4;
int x6__5;
int x6__6;
int x6__7;
int x6__8;
int x6__9;
int x7;
int x7__0;
int x7_0;
int x7_1;
int x7_2;
int x7_3;
int x7_4;
int x7_5;
int x7_6;
int x7_7;
int x7_8;
int x7_9;
int x7__1;
int x7__2;
int x7__3;
int x7__4;
int x7__5;
int x7__6;
int x7__7;
int x7__8;
int x7__9;
int x8;
int x8__0;
int x8_0;
int x8_1;
int x8_2;
int x8_3;
int x8_4;
int x8_5;
int x8_6;
int x8_7;
int x8_8;
int x8_9;
int x8__1;
int x8__2;
int x8__3;
int x8__4;
int x8__5;
int x8__6;
int x8__7;
int x8__8;
int x8__9;
int x9;
int x9__0;
int x9_0;
int x9_1;
int x9_2;
int x9_3;
int x9_4;
int x9_5;
int x9_6;
int x9_7;
int x9_8;
int x9_9;
int x9__1;
int x9__2;
int x9__3;
int x9__4;
int x9__5;
int x9__6;
int x9__7;
int x9__8;
int x9__9;
}
\problem {
\part[left](!(((((x0__1) - (x0__0))) >= (1))) & !(((((x0__2) - (x0__1))) >= (1))) & !(((((x0__3) - (x0__2))) >= (1))) & !(((((x0__4) - (x0__3))) >= (1))) & !(((((x0__5) - (x0__4))) >= (1))) & !(((((x0__6) - (x0__5))) >= (1))) & !(((((x0__7) - (x0__6))) >= (1))) & !(((((x0__8) - (x0__7))) >= (1))) & !(((((x0__9) - (x0__8))) >= (1))) & (!(((((x0_0) - (x0))) >= (1))) | !(((((x1) - (x0__9))) >= (1)))) & !(((((x0_1) - (x0_0))) >= (1))) & !(((((x0_2) - (x0_1))) >= (1))) & !(((((x0_3) - (x0_2))) >= (1))) & !(((((x0_4) - (x0_3))) >= (1))) & !(((((x0_5) - (x0_4))) >= (1))) & !(((((x0_6) - (x0_5))) >= (1))) & !(((((x0_7) - (x0_6))) >= (1))) & !(((((x0_8) - (x0_7))) >= (1))) & !(((((x0_9) - (x0_8))) >= (1))) & !(((((x1) - (x0_9))) >= (1))) & !(((((x1__0) - (x1))) >= (1))) & !(((((x1__1) - (x1__0))) >= (1))) & !(((((x1__2) - (x1__1))) >= (1))) & !(((((x1__3) - (x1__2))) >= (1))) & !(((((x1__4) - (x1__3))) >= (1))) & !(((((x1__5) - (x1__4))) >= (1))) & !(((((x1__6) - (x1__5))) >= (1))) & !(((((x1__7) - (x1__6))) >= (1))) & !(((((x1__8) - (x1__7))) >= (1))) & !(((((x1__9) - (x1__8))) >= (1))) & (!(((((x1_0) - (x1))) >= (1))) | !(((((x2) - (x1__9))) >= (1)))) & !(((((x1_1) - (x1_0))) >= (1))) & !(((((x1_2) - (x1_1))) >= (1))) & !(((((x1_3) - (x1_2))) >= (1))) & !(((((x1_4) - (x1_3))) >= (1))) & !(((((x1_5) - (x1_4))) >= (1))) & !(((((x1_6) - (x1_5))) >= (1))) & !(((((x1_7) - (x1_6))) >= (1))) & !(((((x1_8) - (x1_7))) >= (1))) & !(((((x1_9) - (x1_8))) >= (1))) & !(((((x2) - (x1_9))) >= (1))) & !(((((x2__0) - (x2))) >= (1))) & !(((((x2__1) - (x2__0))) >= (1))) & !(((((x2__2) - (x2__1))) >= (1))) & !(((((x2__3) - (x2__2))) >= (1))) & !(((((x2__4) - (x2__3))) >= (1))) & !(((((x2__5) - (x2__4))) >= (1))) & !(((((x2__6) - (x2__5))) >= (1))) & !(((((x2__7) - (x2__6))) >= (1))) & !(((((x2__8) - (x2__7))) >= (1))) & !(((((x2__9) - (x2__8))) >= (1))) & (!(((((x2_0) - (x2))) >= (1))) | !(((((x3) - (x2__9))) >= (1)))) & !(((((x2_1) - (x2_0))) >= (1))) & !(((((x2_2) - (x2_1))) >= (1))) & !(((((x2_3) - (x2_2))) >= (1))) & !(((((x2_4) - (x2_3))) >= (1))) & !(((((x2_5) - (x2_4))) >= (1))) & !(((((x2_6) - (x2_5))) >= (1))) & !(((((x2_7) - (x2_6))) >= (1))) & !(((((x2_8) - (x2_7))) >= (1))) & !(((((x2_9) - (x2_8))) >= (1))) & !(((((x3) - (x2_9))) >= (1))) & !(((((x3__0) - (x3))) >= (1))) & !(((((x3__1) - (x3__0))) >= (1))) & !(((((x3__2) - (x3__1))) >= (1))) & !(((((x3__3) - (x3__2))) >= (1))) & !(((((x3__4) - (x3__3))) >= (1))) & !(((((x3__5) - (x3__4))) >= (1))) & !(((((x3__6) - (x3__5))) >= (1))) & !(((((x3__7) - (x3__6))) >= (1))) & !(((((x3__8) - (x3__7))) >= (1))) & !(((((x3__9) - (x3__8))) >= (1))) & (!(((((x3_0) - (x3))) >= (1))) | !(((((x4) - (x3__9))) >= (1)))) & !(((((x3_1) - (x3_0))) >= (1))) & !(((((x3_2) - (x3_1))) >= (1))) & !(((((x3_3) - (x3_2))) >= (1))) & !(((((x3_4) - (x3_3))) >= (1))) & !(((((x3_5) - (x3_4))) >= (1))) & !(((((x3_6) - (x3_5))) >= (1))) & !(((((x3_7) - (x3_6))) >= (1))) & !(((((x3_8) - (x3_7))) >= (1))) & !(((((x3_9) - (x3_8))) >= (1))) & !(((((x4) - (x3_9))) >= (1))) & !(((((x4__0) - (x4))) >= (1))) & !(((((x4__1) - (x4__0))) >= (1))) & !(((((x4__2) - (x4__1))) >= (1))) & !(((((x4__3) - (x4__2))) >= (1))) & !(((((x4__4) - (x4__3))) >= (1))) & !(((((x4__5) - (x4__4))) >= (1))) & !(((((x4__6) - (x4__5))) >= (1))) & !(((((x4__7) - (x4__6))) >= (1))) & !(((((x4__8) - (x4__7))) >= (1))) & !(((((x4__9) - (x4__8))) >= (1))) & (!(((((x4_0) - (x4))) >= (1))) | !(((((x5) - (x4__9))) >= (1)))) & !(((((x4_1) - (x4_0))) >= (1))) & !(((((x4_2) - (x4_1))) >= (1))) & !(((((x4_3) - (x4_2))) >= (1))) & !(((((x4_4) - (x4_3))) >= (1))) & !(((((x4_5) - (x4_4))) >= (1))) & !(((((x4_6) - (x4_5))) >= (1))) & !(((((x4_7) - (x4_6))) >= (1))) & !(((((x4_8) - (x4_7))) >= (1))) & !(((((x4_9) - (x4_8))) >= (1))) & !(((((x5) - (x4_9))) >= (1))) & !(((((x5__0) - (x5))) >= (1))) & !(((((x5__1) - (x5__0))) >= (1))) & !(((((x5__2) - (x5__1))) >= (1))) & !(((((x5__3) - (x5__2))) >= (1))) & !(((((x5__4) - (x5__3))) >= (1))) & !(((((x5__5) - (x5__4))) >= (1))) & !(((((x5__6) - (x5__5))) >= (1))) & !(((((x5__7) - (x5__6))) >= (1))) & !(((((x5__8) - (x5__7))) >= (1))) & !(((((x5__9) - (x5__8))) >= (1))) & (!(((((x5_0) - (x5))) >= (1))) | !(((((x6) - (x5__9))) >= (1)))) & !(((((x5_1) - (x5_0))) >= (1))) & !(((((x5_2) - (x5_1))) >= (1))) & !(((((x5_3) - (x5_2))) >= (1))) & !(((((x5_4) - (x5_3))) >= (1))) & !(((((x5_5) - (x5_4))) >= (1))) & !(((((x5_6) - (x5_5))) >= (1))) & !(((((x5_7) - (x5_6))) >= (1))) & !(((((x5_8) - (x5_7))) >= (1))) & !(((((x5_9) - (x5_8))) >= (1))) & !(((((x6) - (x5_9))) >= (1))) & !(((((x6__0) - (x6))) >= (1))) & !(((((x6__1) - (x6__0))) >= (1))) & !(((((x6__2) - (x6__1))) >= (1))) & !(((((x6__3) - (x6__2))) >= (1))) & !(((((x6__4) - (x6__3))) >= (1))) & !(((((x6__5) - (x6__4))) >= (1))) & !(((((x6__6) - (x6__5))) >= (1))) & !(((((x6__7) - (x6__6))) >= (1))) & !(((((x6__8) - (x6__7))) >= (1))) & !(((((x6__9) - (x6__8))) >= (1))) & (!(((((x6_0) - (x6))) >= (1))) | !(((((x7) - (x6__9))) >= (1)))) & !(((((x6_1) - (x6_0))) >= (1))) & !(((((x6_2) - (x6_1))) >= (1))))
 & 
\part[right](!(((((x6_3) - (x6_2))) >= (1))) & !(((((x6_4) - (x6_3))) >= (1))) & !(((((x6_5) - (x6_4))) >= (1))) & !(((((x6_6) - (x6_5))) >= (1))) & !(((((x6_7) - (x6_6))) >= (1))) & !(((((x6_8) - (x6_7))) >= (1))) & !(((((x6_9) - (x6_8))) >= (1))) & !(((((x7) - (x6_9))) >= (1))) & !(((((x7__0) - (x7))) >= (1))) & !(((((x7__1) - (x7__0))) >= (1))) & !(((((x7__2) - (x7__1))) >= (1))) & !(((((x7__3) - (x7__2))) >= (1))) & !(((((x7__4) - (x7__3))) >= (1))) & !(((((x7__5) - (x7__4))) >= (1))) & !(((((x7__6) - (x7__5))) >= (1))) & !(((((x7__7) - (x7__6))) >= (1))) & !(((((x7__8) - (x7__7))) >= (1))) & !(((((x7__9) - (x7__8))) >= (1))) & (!(((((x7_0) - (x7))) >= (1))) | !(((((x8) - (x7__9))) >= (1)))) & !(((((x7_1) - (x7_0))) >= (1))) & !(((((x7_2) - (x7_1))) >= (1))) & !(((((x7_3) - (x7_2))) >= (1))) & !(((((x7_4) - (x7_3))) >= (1))) & !(((((x7_5) - (x7_4))) >= (1))) & !(((((x7_6) - (x7_5))) >= (1))) & !(((((x7_7) - (x7_6))) >= (1))) & !(((((x7_8) - (x7_7))) >= (1))) & !(((((x7_9) - (x7_8))) >= (1))) & !(((((x8) - (x7_9))) >= (1))) & !(((((x8__0) - (x8))) >= (1))) & !(((((x8__1) - (x8__0))) >= (1))) & !(((((x8__2) - (x8__1))) >= (1))) & !(((((x8__3) - (x8__2))) >= (1))) & !(((((x8__4) - (x8__3))) >= (1))) & !(((((x8__5) - (x8__4))) >= (1))) & !(((((x8__6) - (x8__5))) >= (1))) & !(((((x8__7) - (x8__6))) >= (1))) & !(((((x8__8) - (x8__7))) >= (1))) & !(((((x8__9) - (x8__8))) >= (1))) & (!(((((x8_0) - (x8))) >= (1))) | !(((((x9) - (x8__9))) >= (1)))) & !(((((x8_1) - (x8_0))) >= (1))) & !(((((x8_2) - (x8_1))) >= (1))) & !(((((x8_3) - (x8_2))) >= (1))) & !(((((x8_4) - (x8_3))) >= (1))) & !(((((x8_5) - (x8_4))) >= (1))) & !(((((x8_6) - (x8_5))) >= (1))) & !(((((x8_7) - (x8_6))) >= (1))) & !(((((x8_8) - (x8_7))) >= (1))) & !(((((x8_9) - (x8_8))) >= (1))) & !(((((x9) - (x8_9))) >= (1))) & !(((((x9__0) - (x9))) >= (1))) & !(((((x9__1) - (x9__0))) >= (1))) & !(((((x9__2) - (x9__1))) >= (1))) & !(((((x9__3) - (x9__2))) >= (1))) & !(((((x9__4) - (x9__3))) >= (1))) & !(((((x9__5) - (x9__4))) >= (1))) & !(((((x9__6) - (x9__5))) >= (1))) & !(((((x9__7) - (x9__6))) >= (1))) & !(((((x9__8) - (x9__7))) >= (1))) & !(((((x9__9) - (x9__8))) >= (1))) & (!(((((x9_0) - (x9))) >= (1))) | !(((((x10) - (x9__9))) >= (1)))) & !(((((x9_1) - (x9_0))) >= (1))) & !(((((x9_2) - (x9_1))) >= (1))) & !(((((x9_3) - (x9_2))) >= (1))) & !(((((x9_4) - (x9_3))) >= (1))) & !(((((x9_5) - (x9_4))) >= (1))) & !(((((x9_6) - (x9_5))) >= (1))) & !(((((x9_7) - (x9_6))) >= (1))) & !(((((x9_8) - (x9_7))) >= (1))) & !(((((x9_9) - (x9_8))) >= (1))) & !(((((x10) - (x9_9))) >= (1))) & !(((((x10__0) - (x10))) >= (1))) & !(((((x10__1) - (x10__0))) >= (1))) & !(((((x10__2) - (x10__1))) >= (1))) & !(((((x10__3) - (x10__2))) >= (1))) & !(((((x10__4) - (x10__3))) >= (1))) & !(((((x10__5) - (x10__4))) >= (1))) & !(((((x10__6) - (x10__5))) >= (1))) & !(((((x10__7) - (x10__6))) >= (1))) & !(((((x10__8) - (x10__7))) >= (1))) & !(((((x10__9) - (x10__8))) >= (1))) & (!(((((x10_0) - (x10))) >= (1))) | !(((((x11) - (x10__9))) >= (1)))) & !(((((x10_1) - (x10_0))) >= (1))) & !(((((x10_2) - (x10_1))) >= (1))) & !(((((x10_3) - (x10_2))) >= (1))) & !(((((x10_4) - (x10_3))) >= (1))) & !(((((x10_5) - (x10_4))) >= (1))) & !(((((x10_6) - (x10_5))) >= (1))) & !(((((x10_7) - (x10_6))) >= (1))) & !(((((x10_8) - (x10_7))) >= (1))) & !(((((x10_9) - (x10_8))) >= (1))) & !(((((x11) - (x10_9))) >= (1))) & !(((((x11__0) - (x11))) >= (1))) & !(((((x11__1) - (x11__0))) >= (1))) & !(((((x11__2) - (x11__1))) >= (1))) & !(((((x11__3) - (x11__2))) >= (1))) & !(((((x11__4) - (x11__3))) >= (1))) & !(((((x11__5) - (x11__4))) >= (1))) & !(((((x11__6) - (x11__5))) >= (1))) & !(((((x11__7) - (x11__6))) >= (1))) & !(((((x11__8) - (x11__7))) >= (1))) & !(((((x11__9) - (x11__8))) >= (1))) & (!(((((x11_0) - (x11))) >= (1))) | !(((((x12) - (x11__9))) >= (1)))) & !(((((x11_1) - (x11_0))) >= (1))) & !(((((x11_2) - (x11_1))) >= (1))) & !(((((x11_3) - (x11_2))) >= (1))) & !(((((x11_4) - (x11_3))) >= (1))) & !(((((x11_5) - (x11_4))) >= (1))) & !(((((x11_6) - (x11_5))) >= (1))) & !(((((x11_7) - (x11_6))) >= (1))) & !(((((x11_8) - (x11_7))) >= (1))) & !(((((x11_9) - (x11_8))) >= (1))) & !(((((x12) - (x11_9))) >= (1))) & !(((((x12__0) - (x12))) >= (1))) & !(((((x12__1) - (x12__0))) >= (1))) & !(((((x12__2) - (x12__1))) >= (1))) & !(((((x12__3) - (x12__2))) >= (1))) & !(((((x12__4) - (x12__3))) >= (1))) & !(((((x12__5) - (x12__4))) >= (1))) & !(((((x12__6) - (x12__5))) >= (1))) & !(((((x12__7) - (x12__6))) >= (1))) & !(((((x12__8) - (x12__7))) >= (1))) & !(((((x12__9) - (x12__8))) >= (1))) & (!(((((x12_0) - (x12))) >= (1))) | !(((((x13) - (x12__9))) >= (1)))) & !(((((x12_1) - (x12_0))) >= (1))) & !(((((x12_2) - (x12_1))) >= (1))) & !(((((x12_3) - (x12_2))) >= (1))) & !(((((x12_4) - (x12_3))) >= (1))) & !(((((x12_5) - (x12_4))) >= (1))) & !(((((x12_6) - (x12_5))) >= (1))) & !(((((x12_7) - (x12_6))) >= (1))) & !(((((x12_8) - (x12_7))) >= (1))) & !(((((x12_9) - (x12_8))) >= (1))) & !(((((x13) - (x12_9))) >= (1))) & ((((x13) - (x0))) >= (1)) & !(((((x0__0) - (x0))) >= (1))))
 -> false
}
\interpolant{left; right}
